COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 natax.lsp[f81,jmc]	ekl axioms for arithmetic
C00003 ENDMK
C⊗;
;;; natax.lsp[f81,jmc]	ekl axioms for arithmetic

(proof natax)

(decl (m m0 m1 m2 n n0 n1 n2) |ground| variable natnump)

(decl (+) |ground⊗ground→ground| constant nil infix 910)

(decl (*) |ground⊗ground→ground| constant nil infix 920)

(decl (0 1 2 3) |ground| constant natnump)
(decl (natnump) |ground→truthval| constant nil 840)
(axiom |∀n.natnump n|)
(decide |natnump(2)|)
switched to NATAX
* 
* 
* 
* 
* pformat: infix, prefix, unary, infprefix or bindop needed.
* expected another op before N
* decide: cannot prove the following :
NATNUMP(2)
want to assume these?(y or n):